|
| creator |
Göller, Stefan
| | Lohrey, Markus
| | date |
2005-06-24
| | | | description |
38 pages
| |
Hierarchical graph definitions allow a modular description of graphs
using modules for the specification of repeated substructures.
Beside this modularity, hierarchical graph definitions also allow to
specify graphs of exponential size using polynomial size
descriptions. In many cases, this succinctness increases the
computational complexity of decision problems. In this paper, the
model-checking problem for the modal $\mu$-calculus and (monadic)
least fixpoint logic on hierarchically defined input graphs is
investigated. In order to analyze the modal $\mu$-calculus, parity
games on hierarchically defined input graphs are investigated. In
most cases precise upper and lower complexity bounds are derived. A
restriction on hierarchical graph definitions that leads to more
efficient model-checking algorithms is presented.
| | format |
application/pdf
| | 321585 Bytes | |